(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun Jsnkj_new () Real)
(declare-fun d () Real)
(declare-fun t () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun h () Real)
(declare-fun g () Real)
(declare-fun i () Real)
(declare-fun j () Real)
(declare-fun l () Real)
(declare-fun k () Real)
(declare-fun m () Real)
(declare-fun n () Real)
(declare-fun o () Real)
(declare-fun p () Real)
(declare-fun q () Real)
(declare-fun r () Real)
(declare-fun t17uscore0dollarskuscore1_shifted () Real)
(declare-fun s () Real)
(declare-fun v () Real)
(assert (not (=> (and (=> (<= 0.0 (- d k) t17uscore0dollarskuscore1_shifted) (and (<= 0.0 (* (- Jsnkj_new l) (- d k))) (<= m n 0 (- b i)))) (< (+ (+ g (/ 0 (* 2.0 (- Jsnkj_new l)))) (* (+ (- (- j) (- Jsnkj_new l)) 1.0) (+ (* (* (- c j) (/ 1 2)) (* (- b i)) (- t m))))) (- f o)) (<= 0.0 (- t m)) (<= 0 (/ 81 e n)) (< 0.0 (- Jsnkj_new l)) (>= 0.0 c) (< 0.0 (- e n)) (< 0.0 (- b i))) (< (- f o) (* (/ 1 2) (+ (* t17uscore0dollarskuscore1_shifted t17uscore0dollarskuscore1_shifted) (* t17uscore0dollarskuscore1_shifted (- t m))))) (< (+ (+ (* (- 1.0) (- Jsnkj_new l) t17uscore0dollarskuscore1_shifted t17uscore0dollarskuscore1_shifted) (* t17uscore0dollarskuscore1_shifted (- t m)) g) (/ (* (+ (* l t17uscore0dollarskuscore1_shifted) (- t m)) (+ (* (* (- 1.0) (- Jsnkj_new l)) t17uscore0dollarskuscore1_shifted) (- t m))) (* 2.0 (- Jsnkj_new l)))) 0))))
(assert (= a (mod h p)))
(assert (= c (+ j q r m v)))
(assert (= e (+ n s)))
(check-sat)
